Inference at * 2 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
  (f^n+m(x)) ~ (f^n(do-apply(f^m;x))) 

latex

 by CaseNat 0 `n' 

latex

 1: 

 1: 9. n = 0
 1:   (f^0+m(x)) ~ (f^0(do-apply(f^m;x)))
 2: 

 2: 9. (n = 0)
 2:   (f^n+m(x)) ~ (f^n(do-apply(f^m;x)))
 .

Definitions	Dec(P), P  Q, left + right, x:AB(x), , {x:A| B(x)} , A  B, A, False, s ~ t, , s = t, t  T, , SQType(T), x:A. B(x), P  Q, {T}
Lemmas	decidable int equal